Nuprl Lemma : comp_nat_ind_tp
9,38
postcript
pdf
P
:(
{k}). (
i
:
. (
j
:
. (
j
<
i
)
P
(
j
))
P
(
i
))
{
i
:
.
P
(
i
)}
latex
ProofTree
Definitions
t
T
,
{
T
}
,
x
(
s
)
,
P
Q
,
,
x
:
A
.
B
(
x
)
,
False
,
A
,
A
B
,
i
j
,
Lemmas
nat
wf
,
ge
wf
,
nat
properties
,
le
wf
origin
P:(
{k}). (i:. (j:. (j < i) 
P(j)) P(i)) {i:. P(i)}
P:({k}). (i:. (j:. (j < i) P(j)) P(i)) {i:. P(i)}
T Qx:A. B(x)
A
B
j